(0) Obligation:
Clauses:
d(+(U, V), X, +(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(-(U, V), X, -(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(!, ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU)))).
d(-(U), X, -(DU)) :- ','(!, d(U, X, DU)).
d(exp(U), X, *(exp(U), DU)) :- ','(!, d(U, X, DU)).
d(log(U), X, /(DU, U)) :- ','(!, d(U, X, DU)).
d(X, X, 1) :- !.
d(C, X, 0).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).
Query: deriv(g,g,a)
(1) CutEliminatorProof (SOUND transformation)
Eliminated all cuts by simply ignoring them[PROLOG].
(2) Obligation:
Clauses:
d(+(U, V), X, +(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(-(U, V), X, -(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(d(U, X, DU), d(V, X, DV)).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2))) :- ','(d(U, X, DU), d(V, X, DV)).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU))).
d(-(U), X, -(DU)) :- d(U, X, DU).
d(exp(U), X, *(exp(U), DU)) :- d(U, X, DU).
d(log(U), X, /(DU, U)) :- d(U, X, DU).
d(X, X, 1).
d(C, X, 0).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).
Query: deriv(g,g,a)
(3) UndefinedPredicateHandlerProof (SOUND transformation)
Added facts for all undefined predicates [PROLOG].
(4) Obligation:
Clauses:
d(+(U, V), X, +(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(-(U, V), X, -(DU, DV)) :- ','(d(U, X, DU), d(V, X, DV)).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(d(U, X, DU), d(V, X, DV)).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2))) :- ','(d(U, X, DU), d(V, X, DV)).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU))).
d(-(U), X, -(DU)) :- d(U, X, DU).
d(exp(U), X, *(exp(U), DU)) :- d(U, X, DU).
d(log(U), X, /(DU, U)) :- d(U, X, DU).
d(X, X, 1).
d(C, X, 0).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).
integer(X0).
is(X0, X1).
write(X0).
Query: deriv(g,g,a)
(5) PrologToPiTRSProof (SOUND transformation)
We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
R is empty.
Pi is empty.
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(6) Obligation:
Pi-finite rewrite system:
R is empty.
Pi is empty.
(7) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(8) YES